A power function is a function of the form xt where t is a constant real number and x is a variable. Examples of power functions include, but are not limited to
      1    x    ,      x    ,            1              x              ⁢                  ⁢    and    ⁢                  ⁢                  x                  2          3                    .      
A hardware implementation of a power function uses a specific number representation, such as, but not limited to, a fixed point number representation or a floating point representation, to perform the power function. As is known to those skilled in the art a fixed point number representation has a fixed number of digits after the radix point (e.g. decimal point or binary point). In contrast, a floating point number representation does not have a fixed radix point (i.e. it can “float”). In other words the radix point can be placed anywhere within the representation.
The most common floating point standard is the Institute of Electrical and Electronics Engineers (IEEE) standard for floating-point arithmetic (IEEE-754). IEEE-754 specifies that floating point numbers are represented by three numbers: sign, exponent and mantissa (s, exp, mant). In general the three numbers (s, exp, mant) are interpreted, for a fixed integer bias, as shown in equation (1):(−1)s2exp-bias1·mant  (1)
IEEE-754 defines the four basic formats shown in Table 1 for floating point numbers with varying degrees of precision. In particular, they are encoded with 16, 32, 64 and 128 bits respectively.
TABLE 1ExponentMantissaRoundoffSignWidthWidthBiasErrorTypeNameWidth(ew)(mw)2ew−1 − 1(u)HalfF161510152−11SingleF3218231272−24DoubleF641115210232−53QuadF12811511216383 2−113
A property (e.g. error requirement) of a hardware design to implement a power function may be verified via formal verification or simulation-based verification. Formal verification is a systematic process that uses mathematical reasoning to verify a property in a hardware design. In contrast, simulation-based verification is a process in which a hardware design is tested by applying stimuli to the hardware design and monitoring the output of the hardware design in response to the stimuli.
Formal verification can improve controllability as compared to simulation based verification. Low controllability occurs when the number of simulation test signals or vectors required to thoroughly simulate a hardware design becomes unmanageable. For example, a 32-bit comparator requires 264 test vectors. This would take millions of years to verify exhaustively by simulation based verification. By performing formal verification, the 32-bit comparator can be verified in less than a minute.
While formal verification can provide advantages over simulation-based verification, hardware designs to implement power functions using a floating point number representation (which are referred to herein as floating point power functions), especially those that have an allowable error (so that many possible output values are valid for the same input), are difficult to verify using formal verification due to their complexity. Accordingly, hardware designs to implement floating point power functions are typically verified through simulation-based verification. However, exhaustive simulation (i.e. testing each possible input) takes a long time, and random simulation (i.e. testing a random subset of possible inputs) is prone to error.
The embodiments described below are provided by way of example only and are not limiting of implementations which solve any or all of the disadvantages of known verification methods.